def val_is_var(val):
    return type(val) is str and (val[0].isupper() or val[0] == '_')

def val_is_const(val):
    return type(val) is str and val[0].islower()

fake_var_cnt = 0
def fake_var():
    global fake_var_cnt
    var = '_' + str(fake_var_cnt)
    fake_var_cnt += 1
    return var                

def unify_not_var(left, right, lbinds, rbinds):
    if type(left) is not type(right):
        return False   
    # constants
    if val_is_const(left):
        return left == right
    # lists
    if type(left) is not list:
        return False
    if len(left) != len(right):
        return False
    for new_left, new_right in zip(left, right):
        if not unify(new_left, new_right, lbinds, rbinds):
            return False
    return True

def propgate(var, val, lbinds, rbinds):
    if var in lbinds:
        propgate(lbinds[var], val, lbinds, rbinds)
        del lbinds[var]
    if var in rbinds:
        propgate(rbinds[var], val, lbinds, rbinds)
        del rbinds[var]
    for key, value in lbinds.items():
        if value == var:
            lbinds[key] = val
    for key, value in rbinds.items():
        if value == var:
            rbinds[key] = val
    
    

def unify(left, right, lbinds, rbinds):
    if not val_is_var(left):
        if not val_is_var(right):
            return unify_not_var(left, right, lbinds, rbinds)
        if not right in rbinds:
            rbinds[right] = left
            return True
        if not val_is_var(rbinds[right]):
            return unify_not_var(left, rbinds[right], lbinds, rbinds)
        propgate(rbinds[right], left, lbinds, rbinds)
        return True
    if not left in lbinds:
        if not val_is_var(right):
            lbinds[left] = right
            return True
        if not right in rbinds:
            lbinds[left] = rbinds[right] = fake_var()
            return True
        lbinds[left] = rbinds[right]
        return True
    if not val_is_var(lbinds[left]):
        if not val_is_var(right):
            return unify_not_var(lbinds[left], right, lbinds, rbinds)
        if not right in rbinds:
            rbinds[right] = lbinds[left]
            return True
        if not val_is_var(rbinds[right]):
            return unify_not_var(lbinds[left], rbinds[right], lbinds, rbinds)
        propgate(rbinds[right], lbinds[left], lbinds, rbinds)
        return True
    if not val_is_var(right):
        propgate(lbinds[left], right, lbinds, rbinds)
        return True
    if not right in rbinds:
        rbinds[right] = lbinds[left]
        return True
    # if not val_is_var(rbinds[right]):
    #     return propagate(lbinds[left], rbinds[right], lbinds, rbinds)

    propagate(lbinds[left], rbinds[right], lbinds, rbinds)
    return True

class Search:
    def __init__(self, base, query):
        self.query = query
        self.place = iter(base)
        self.up_binds = None
        self.scope = None

    def scope_bind(self):
        new_binds = {}
        for key, value in self.up_binds.items():
            new_binds[key] = self.scope.bind(value)
        return new_binds

    def get(self, base):
        if self.scope is not None:
            if self.scope.run(base):
                return self.scope_bind()
            self.up_binds = None
            self.scope = None
            
        for fact in self.place:
            rbinds = {}
            lbinds = {}
            if unify(self.query, fact[0], lbinds, rbinds):
                if len(fact[1]) == 0:
                    return lbinds
                scope = Scope(base, fact[1], rbinds)
                if scope.run(base):
                    self.up_binds = lbinds
                    self.scope = scope
                    return self.scope_bind()
        return False

class Scope:
    def __init__(self, base, queries, binds={}):
        self.final = None
        self.queries = queries
        self.sbinds = [binds]
        self.searches = [Search(base, self.bind(queries[0]))]

    def resl_var(self, var):
        for binds in self.sbinds:
            if var in binds:
                var = binds[var]
        if self.final is not None:
            if var in self.final:
                var = self.final[var]
        return var

    def resl_list(self, query):
        new = []
        for val in query:
            new.append(self.bind(val))
        return new

    def bind(self, query):
        if val_is_const(query):
            return query
        if val_is_var(query):
            return self.resl_var(query)
        return self.resl_list(query)

    def latest_query(self):
        return self.bind(self.queries[len(self.searches)])

    def run(self, base):
        self.final = None
        while True:
            binds = self.searches[-1].get(base)
            if binds is False:
                self.sbinds.pop()
                self.searches.pop()
                if len(self.searches) == 0:
                    return False
            elif len(self.searches) == len(self.queries):
                self.final = binds
                return True
            else:
                self.sbinds.append(binds)
                self.searches.append(Search(base, self.latest_query()))
        
        

lbinds = {}
rbinds = {}
# unify(['A', 'b', 'C', 'E', 'A'], ['B', 'B', 'B', 'D', 'D'], lbinds, rbinds)
# print(lbinds)
# print(rbinds)

base = [
    [['human', 'Y'],       [['woman', 'Y']] ],
    [['man', 'socrates'],  []               ],
    [['human', 'X'],       [['man', 'X']]   ],
    [['woman', 'ophelia'], []               ],
    [['mortal', 'Z'],      [['human', 'Z']] ],
]

search = Search(base, ['X', 'socrates'])
result = search.get(base)
while result is not False:
    print(result)
    result = search.get(base)
